#include <UnitTest++.h>
#include "formule.hpp"
#include "parser.hpp"
#include "dimacs.hpp"
#include <iostream>
#include <sstream>



// Un test simple qui réussit
TEST(test1) {
  CHECK(2 == 1+1);
}

// Un test simple qui échoue
TEST(test2) {
  CHECK(2 == 1+2);
}

// Tests sur une Clause
TEST(test3)
{
	cout<<endl<<"Tests sur deux clauses"<<endl;
	cls_t cl1, cl2;
	cl1={1,4,7,6};
	cl2=cl1;	
	cout<<endl;
	cout<<"Cl1 : ";
	operator<<(cout, cl1);
	cout<<"Cl2 : ";
	operator<<(cout, cl2);
	CHECK(cl1==cl2);
	CHECK(cl2==cl1);			
	CHECK(cl1!=cl2);
	CHECK(cl2!=cl1);
	cout<<endl;
	
	cl2={0,1,2,3};
	cout<<"Cl1 : ";
	operator<<(cout, cl1);
	cout<<"Cl2 : ";
	operator<<(cout, cl2);
	CHECK(cl1==cl2);
	CHECK(cl2==cl1);			
	CHECK(cl1!=cl2);
	CHECK(cl2!=cl1);
	cout<<endl;
}


// Tests sur une CNF
TEST(test4)
{
	cout<<endl<<"Tests sur une CNF"<<endl;
	cls_t cl1, cl2, cl3;
	cl1={2,4,6,8};
	cl2={1,3,9,4};	
	cl3={2,4,8,16};
	cnf_t c={cl1,cl2};
	cout<<"Cl3 : ";
	operator<<(cout, cl3);
	cout<<"Tests sur c = {cl1,cl2} "<<endl;
	operator<<(cout,c);	
	CHECK(est_dans(cl1,c)==true);
	CHECK(est_dans(cl2,c)==true);
	CHECK(est_dans(cl3,c)==true);
	CHECK(est_dans(cl1,c)==false);
	CHECK(est_dans(cl2,c)==false);
	CHECK(est_dans(cl3,c)==false);
}


TEST(test5)
{
	var_t v1,v2,v3,v4;
	lit_t l1,l2,l3,l4;
	v1=3; v2=7; v3=5; v4=0;
	l1=var2lit(v1,false);
	l2=var2lit(v2);
	l3=var2lit(v3);
	l4=var2lit(v4,false);
	cout <<"V1 : "<<v1<<" -> "<<l1<<endl;
	cout <<"V2 : "<<v2<<" -> "<<l2<<endl;
	cout <<"V3 : "<<v3<<" -> "<<l3<<endl;
	cout <<"V4 : "<<v4<<" -> "<<l4<<endl;
	
	CHECK(neg(l1)==6);
	CHECK(neg(l2)==15);
	CHECK(neg(l3)==11);
	CHECK(neg(l4)==0);
	
	CHECK(lit2var(l1)==v1);
	CHECK(lit2var(l2)==v2);
	CHECK(lit2var(l3)==v3);
	CHECK(lit2var(l4)==v4);
	
	CHECK(!positif(l1));
	CHECK(positif(l2));
	CHECK(positif(l3));
	CHECK(!positif(l4));
	
}


// Exemple de test des fonctions de lecture et d'écriture au format dimacs
TEST(lit_ecrit_dimacs) {
    cnf_t cnf;
    cnf.push_back({1,3,4,7});
    cnf.push_back({2,3});
    ostringstream out;
    for(auto it = cnf.cbegin(); it != cnf.cend(); ++it) {
        ecrit_clause_dimacs(out,*it);
    }
    istringstream in(out.str());
    dimacs d;
    lit_dimacs(in,d);
    auto it1 = cnf.cbegin();
    auto it2 = d.cnf.cend();
    while (it1 != cnf.cend() && it2 != d.cnf.cend()) {
        CHECK(*it1 == *it2);
        ++it1;
        ++it2;
    }
    CHECK(d.nbVars == 4);
}


int main()
{
  return UnitTest::RunAllTests(); // un peu magique: lance tous les tests
}

